open import Data.Product using ( _×_ ; _,′_ ) 
open import Data.Sum.Base using ( _⊎_ ; [_,_]′ ; inj₁ ; inj₂)
import Relation.Binary.EqReasoning as EqR
open import Algebra using ( CommutativeRing )
open import Algebra.Structures using ( IsCommutativeRing )
open import Relation.Binary using ( Rel )
open import Algebra.FunctionProperties using ( Op₁ ; Op₂ ; Inverse ; Congruent₁ )
open import Level using ( Level ; _⊔_ ; suc )
open import Relation.Nullary using ( ¬_ )



module Lemma-VI-1-7 where

open import Function

{-- z książki: 
rf e is an idempotent in a local ring, then either e is a unit, in
which case e
1, or 1 - e is a unit, i.n vlhich case e = 0
By an impotent
ring we mean a commutative ring with no nilpotent elements, such that any
idempotent is either 0 or 1.
commutative
local
ring with
no
nilpotents is impotent.

str 141, rozdział VI o ciałach:
Reca1l that a commutative ring E is impotent if
(i) a^n = 0 for some n E N imp1ies a= 0,
and
(ii) a^2 = a implies a = 0 or a = 1.

Condition (i), which is equivalent to a 2 = 0 imp1ies a = 0, says that E
has no nilpotent elements. Condition (ii) says that E has no idempotent
elements other than 0 and 1.

Semiring.agda definiuje _^_
--}

record IsImpotentCommutativeRing {a ℓ : Level} {A : Set a} (_≈_ : Rel A ℓ) 
                          (+ * : Op₂ A)
                          (- : Op₁ A)
                          (0# 1# : A): (Set (a ⊔ ℓ)) where
    field
      isCommutativeRing : IsCommutativeRing  _≈_ + * - 0# 1#
      noNillpotent : (a : A) → (* a a) ≈ 0# → a ≈ 0#
      noIdempotent : (a : A) → (* a a) ≈ a → (a ≈ 0#) ⊎ (a ≈ 1#)
    open IsCommutativeRing isCommutativeRing public
       
record ImpotentCommutativeRing c ℓ : Set (suc (c ⊔ ℓ)) where
  infix  8 -_
  infixl 7 _*_
  infixl 6 _+_
  infix  4 _≈_
  field
    Carrier           : Set c
    _≈_               : Rel Carrier ℓ
    _+_               : Op₂ Carrier
    _*_               : Op₂ Carrier
    -_                : Op₁ Carrier
    0#                : Carrier
    1#                : Carrier
    isImpotentCommutativeRing : IsImpotentCommutativeRing _≈_ _+_ _*_ -_ 0# 1#  

  open IsImpotentCommutativeRing isImpotentCommutativeRing public

  commutativeRing : CommutativeRing _ _
  commutativeRing = record { isCommutativeRing  = isCommutativeRing }


{--
str 151 łatwy lemat 1.7
1.7~.
Let a und b be elements of an impotent ring such that a + b = 1 and ab = O.
Then ei.ther a = 0 and b = 1, or a = 1 and b = O.
PROOF. Multiplying the equation a + b = 1 by b, and making use of the
fact that ab = 0, we obtain b 2 = b. As the ring is impotent, it follows
that b = 0 or b = 1.
--}
Lemma-VI-1-7 : {a ℓ : Level} (icRing : ImpotentCommutativeRing a ℓ) →
             let open ImpotentCommutativeRing icRing in
             (a b : Carrier)
             (a+b=1 : (a + b) ≈ 1#)
             (a∙b=0 : (a * b) ≈ 0#) →
                    (((a ≈ 0#) × (b ≈ 1#)) ⊎  ((a ≈ 1#) × (b ≈ 0#)))
Lemma-VI-1-7 icRing a b a+b=1 a∙b=0 = let open ImpotentCommutativeRing icRing in let open EqR setoid in
  let
      b∙b=b : b * b ≈ b
      b∙b=b = begin
        b * b ≈⟨ sym (+-identityˡ (b * b)) ⟩
        0# + b * b      ≈⟨ +-cong (sym a∙b=0) refl  ⟩
        (a * b) + b * b ≈⟨ sym (distribʳ b a b) ⟩
        (a + b) * b     ≈⟨ *-cong a+b=1 refl ⟩
        1# * b          ≈⟨ *-identityˡ b ⟩
        b               ∎
      b-eq-0-or-1 : (b ≈ 0#) ⊎ (b ≈ 1#)
      b-eq-0-or-1 = noIdempotent b b∙b=b
      b=0-to-a=1 : (b ≈ 0#) → (a ≈ 1#) 
      b=0-to-a=1 b=0 = begin
        a      ≈⟨ sym (+-identityʳ a) ⟩
        a + 0# ≈⟨ +-cong refl(sym b=0) ⟩
        a + b  ≈⟨ a+b=1 ⟩
        1#     ∎
      b=1-to-a=0 : (b ≈ 1#) → (a ≈ 0#)
      b=1-to-a=0 b=1 = begin
        a      ≈⟨ sym (*-identityʳ a) ⟩ 
        a * 1# ≈⟨ *-cong refl (sym b=1) ⟩
        a * b  ≈⟨ a∙b=0 ⟩
        0#     ∎
      in [ (λ b=0 → inj₂ (b=0-to-a=1 b=0 ,′ b=0)) , (λ b=1 → inj₁ ((b=1-to-a=0 b=1) ,′ b=1)) ]′ b-eq-0-or-1

-- Dodatkowe dziadostwo, do wyrzucenia kiedyś
InverseForNonZero : {a ℓ : Level} {A : Set a} (_≈_ : Rel A ℓ) →
  A → A → Op₁ A → Op₂ A → Set (a ⊔ ℓ)
InverseForNonZero  _≈_ 0# 1# _⁻¹ _∙_ = ∀ a → (Inverse _≈_ 1# _⁻¹ _∙_) ⊎ (a ≈ 0#)

{-- DEFINICJA CIAŁA --
Z książki:
  Str 42: A field is a commutative division ring.
    A ring k is a division ring if, for each a and b in k
      a != b if and only if a - b is a unit.
Uwagi dot. definicji:
* nie dopuszcza zerowego pierścienia

Ta definicja *wydaje* mi się niweygodna bo wymaga podawania dowodu że element nie jest równy zeru
(czegoś w stylu `∀ a → a ≢ 0# → Inverse a _`)

Zastosowałem definicję z UniMath:
https://github.com/UniMath/UniMath/blob/master/UniMath/Algebra/Domains_and_Fields.v
```
Definition isafield (X : commring) : UU :=
(isnonzerorig X) × (∏ x : X, (multinvpair X x) ⨿ (x = 0)).
```
Pytanie: czy ta definicja jest równoważna?
Podejrzane jest że ona nie zabrania odwracalności zera!
Ale na szczęśnie nie istnieje ciało z odwracalnym zerem (podane bez dowodu 2/10):
https://en.wikipedia.org/wiki/Unit_(ring_theory)
The set of units of any ring is closed under multiplication (the product of two units is again a unit), and forms a group for this operation. It never contains the element 0 (except in the case of the zero ring), and is therefore not closed under addition; its complement however might be a group under addition, which happens if and only if the ring is a local ring. 
albo tu https://en.wikipedia.org/wiki/Ring_%28mathematics%29:
If 0 = 1 in a ring R (or more generally, 0 is a unit element), then R has only one element, and is called the zero ring.
--}
record IsField {a ℓ} {A : Set a} (_≈_ : Rel A ℓ)
  (+ * : Op₂ A)
  (- ⁻¹ : Op₁ A)
  (0# 1# : A) : Set (a ⊔ ℓ) where
  field
    isCommutativeRing : IsCommutativeRing _≈_ + * - 0# 1#
    isNonZeroRing : ¬ (0# ≈ 1#)
    inverseForNonZero : InverseForNonZero _≈_ 0# 1# ⁻¹ * 
    ⁻¹-cong   : Congruent₁ _≈_ ⁻¹
    
  open IsCommutativeRing isCommutativeRing public
  
record Field c ℓ : Set (suc (c ⊔ ℓ)) where
  infix  9 _⁻¹
  infix  8 -_
  infixl 7 _*_
  infixl 6 _+_
  infix  4 _≈_
  field
    Carrier           : Set c
    _≈_               : Rel Carrier ℓ
    _+_               : Op₂ Carrier
    _*_               : Op₂ Carrier
    -_                : Op₁ Carrier
    _⁻¹               : Op₁ Carrier
    0#                : Carrier
    1#                : Carrier
    isField : IsField _≈_ _+_ _*_ -_ _⁻¹ 0# 1#  

  open IsField isField public

  commutativeRing : CommutativeRing _ _
  commutativeRing = record { isCommutativeRing  = isCommutativeRing } 

